$\forall$$A$, $B$:Type. ($A$ $\subseteq$r $B$) $\Rightarrow$ ($\forall$$x$, $y$:$A$. ($x$ = $y$ $\in$ $B$) $\Rightarrow$ ($x$ = $y$)) $\Rightarrow$ EqDecider($B$) $\subseteq$ EqDecider($A$)